Issue3566-2.agda:12,8-9
(r : R) → A !=< A
when checking that the expression b has type A
